The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

\(x, x) → e
/(x, x) → e
.(e, x) → x
.(x, e) → x
\(e, x) → x
/(x, e) → x
.(x, \(x, y)) → y
.(/(y, x), x) → y
\(x, .(x, y)) → y
/(.(y, x), x) → y
/(x, \(y, x)) → y
\(/(x, y), x) → y

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

\(z0, z0) → e
\(e, z0) → z0
\(z0, .(z0, z1)) → z1
\(/(z0, z1), z0) → z1
/(z0, z0) → e
/(z0, e) → z0
/(.(z0, z1), z1) → z0
/(z0, \(z1, z0)) → z1
.(e, z0) → z0
.(z0, e) → z0
.(z0, \(z0, z1)) → z1
.(/(z0, z1), z1) → z0

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

\, /, .

Defined Pair Symbols:none

Compound Symbols:none

(3) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(4) BOUNDS(O(1), O(1))